Supporting concurrent access to data structures is crucial for the performance of multithreaded programs in shared-memory multiprocessor environments. This motivates programmers to create objects with fewer safety mechanisms (such as locks, which impose a performance overhead) to achieve greater concurrency. However, greater concurrency also increases the difficulty of verifying correctness of the concurrent data structure and the operations performed on the concurrent data structure. Many techniques have been proposed for verifying concurrent data structures, but are not scalable, and often are restricted to a few threads and a few operations. Model checking has been used for verifying concurrent data structures relative to the correctness condition ‘linearizability’.